COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		Source language
C00003 00003			Interpteter for source language
C00005 00004	Notes:
C00006 00005	Theorem
C00007 00006	Try it:
C00010 ENDMK
C⊗;
	Source language
Concrete
exp	::= var | const | sum

sum	::= exp + exp

Abstract
exp	::= var | const | sum

sum	::= struct[ arg1:exp; arg2:exp]


	Object language
Concrete
prog	::= inst prog
	::= ε

inst	::= li | lo | st | ad

li	::= <LI int>

lo	::= <LO adr>

st	::= <ST adr>

ad	::= <AD adr>

adr	::= id

Abstract
prog	::= seq[inst]

inst	::= li 
	::= lo 
	::= st 
	::= ad

li	::= struct[cnst:arg]

lo	::= struct[loc:adr]

		Interpteter for source language

value_s[e:exp;a:environ_s]int
 generic(e)
	[var]      => find(e,a)
	[const]    => denote(e)
	[sum(u,v)] => +(value_s(u,a),value_s(v,a))
 end;



		Interpreter for object language

value_o[p:prog;st:environ_o]environ_o
 on(p)
	[ε]      => st
	[(i⊗p1)] => value_o(p1,step(i,st))
 end;

step[i:inst; st:environ_o] environ_o
 generic(i)
	[li(c)]   => new_env_o(AC,c,st)
	[lo(adr)] => new_env_o(AC,cont(adr),st)
	[st(adr)] => new_env_o(adr,cont(AC),st)
	[ad(adr)] => new_env_o(AC,cont(AC)cont(adr),st)
end;



		Compiler

compile[e:exp;tbl:environ_o]prog
 generic(e)
	[var]      => lo(loc(e,tbl)) 
	[const]    => li(denote e) 
	[sum(u,v)] =>  prog(compile(u,tbl),
			    st(last(nev(tbl)),
			    compile(v,nev(tbl)),
			    ad(last(nev(tbl))))
end;
Notes:
	3.1-3.7 of McCarthy Painter are consequences of  data structures.
	3.13 is also consequence.

	It seemed artificial to use map and t of Mc Carthy Painter.
	 We will see how proof goes.
Theorem

value_o(compile(e:exp,tbl:environ_o),tbl:environ_o) 

	=
		new_env_o(AC,value_s(e:exp,a:environ_s)tbl:environ_o)



Try it:

value_o(						;tbl:environ_o)
	compile[e:exp;tbl:environ_o]prog
	 generic(e)
		[var]      => lo(loc(e,tbl)) 
		[const]    => li(denote e) 
		[sum(u,v)] =>  prog(compile(u,tbl),
				    st(last(nev(tbl)),
				    compile(v,nev(tbl)),
				    ad(last(nev(tbl))))
	end;


equals

new_env_o(AC,					 ,tbl:environ_o)
	      value_s[e:exp;a:environ_s]int
		generic(e)
	 	  [var]      => find(e,a)
		  [const]    => denote(e)
		  [sum(u,v)] => +(value_s(u,a),value_s(v,a))
		end;


Proof is generic on e;

i. [const]
value_o(prog(li(denote(e)),tbl)
value_o(li(denote(e)),tbl)
value_o(ε,step(denote(e),tbl)
new_env_o(AC,denote(e),tbl)


ii. [var]
value_o(prog(lo(loc(e,tbl))),tbl)

step(lo(loc(e)tbl)
new_env_o(AC,cont(loc(e,tbl)),tbl)

?new_env_o(AC,find(e,a),tbl))?


iii.
[sum(u,v)]
value_o(prog(compile(u,tbl),             ,tbl)
  	     st(last(nev(tbl)),
	     compile(v,nev(tbl)),
	     ad(last(nev(tbl))))

value_o(prog(st(last(nev(tbl),             ,step(compile(u,tbl)))
	     compile(v,nev(tbl)),
	     ad(last(nev(tbl))))

value_o(prog(compile(v,nev(tbl))	 ,step(st(last(nev(tbl),step(compile(u,tbl)))
	     ad(last(nev(tbl))))

value_o(prog(                   ,step(compile(v,nev(tbl)),step(st(last(nev(tbl),step(compile(u,tbl)))
	     ad(last(nev(tbl))))

step(ad(last(nev(tbl)))),
     step(compile(v,nev(tbl)),
          step(st(last(nev(tbl),
               step(compile(u,tbl))))))))

Assume theorem for u and v;
	value_o(compile(e:exp,tbl:environ_o),tbl:environ_o) 
			=
	new_env_o(AC,value_s(e:exp,a:environ_s)tbl:environ_o)